Iof proof for Lemma append overlapping sublists:
1. T : Type
2. L1 : T List
3. L2 : T List
4. L : T List
5. x : T
6.
i, j:
. (i < ||L||) 
(j < ||L||) (
(i = j)) ((L[i] = L[j]))
7. f1 : {0..||L1 @ [x]||
}
{0..||L||}
8. increasing(f1;||L1 @ [x]||)
9.
j:{0..||L1 @ [x]||}. (L1 @ [x])[j] = L[(f1(j))]
10. f : {0..(||L2||+1)
}{0..||L||}
11. increasing(f;||L2||+1)
12.
j:{0..(||L2||+1)}. [x / L2][j] = L[(f(j))]
f:{0..||L1 @ [x / L2]||}{0..||L||}
(increasing(f;||L1 @ [x / L2]||)
& (j:{0..||L1 @ [x / L2]||}. (L1 @ [x / L2])[j] = L[(f(j))]))
by Assert ||L1 @ [x / L2]|| = ||L1||+||L2||+1
